0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 588 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 2141 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 24 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 4 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 337 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 360 ms)
↳18 QDP
↳19 QDPOrderProof (⇔, 4652 ms)
↳20 QDP
↳21 DependencyGraphProof (⇔, 0 ms)
↳22 QDP
↳23 UsableRulesProof (⇔, 0 ms)
↳24 QDP
↳25 QReductionProof (⇔, 0 ms)
↳26 QDP
↳27 QDPSizeChangeProof (⇔, 0 ms)
↳28 YES
DB_IN_GGA(s(X1), s(X1), 0) → U3_GGA(X1, isnumberA_in_g(X1))
DB_IN_GGA(s(X1), s(X1), 0) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(s(X1)) → U1_G(X1, isnumberA_in_g(X1))
ISNUMBERA_IN_G(s(X1)) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(p(X1)) → U2_G(X1, isnumberA_in_g(X1))
ISNUMBERA_IN_G(p(X1)) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(p(X1), p(X1), 0) → U4_GGA(X1, isnumberA_in_g(X1))
DB_IN_GGA(p(X1), p(X1), 0) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U5_GGA(X1, X2, X3, X4, dB_in_gga(X1, times(X1, X2), X4))
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → DB_IN_GGA(X1, times(X1, X2), X4)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U6_GGA(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
U6_GGA(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U7_GGA(X1, X2, X3, X4, dB_in_gga(X2, times(X1, X2), X3))
U6_GGA(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(div(X1, X2), div(X1, X2), X3) → U8_GGA(X1, X2, X3, dB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
DB_IN_GGA(div(X1, X2), div(X1, X2), X3) → DB_IN_GGA(times(X1, power(X2, p(0))), div(X1, X2), X3)
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U9_GGA(X1, X2, X3, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U10_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U10_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U11_GGA(X1, X2, X3, dB_in_gga(X1, power(X1, X2), X3))
U10_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2), X3)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U12_GGA(X1, X2, X3, isnumberA_in_g(X1))
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U13_GGA(X1, X2, X3, isnumbercA_in_g(X1))
U13_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → U14_GGA(X1, X2, X3, dB_in_gga(X2, times(X1, X2), X3))
U13_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U15_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X1, times(times(X1, X2), X3), X6))
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → DB_IN_GGA(X1, times(times(X1, X2), X3), X6)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U16_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U17_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X2, times(times(X1, X2), X3), X5))
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → DB_IN_GGA(X2, times(times(X1, X2), X3), X5)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U20_GGA(X1, X2, X3, X4, X5, dB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U21_GGA(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
U21_GGA(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U22_GGA(X1, X2, X3, X4, X5, dB_in_gga(X3, times(div(X1, X2), X3), X4))
U21_GGA(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(div(X1, X2), X3), X4)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U23_GGA(X1, X2, X3, X4, X5, isnumberA_in_g(X2))
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U24_GGA(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U25_GGA(X1, X2, X3, X4, X5, dB_in_gga(X1, times(power(X1, X2), X3), X5))
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, times(power(X1, X2), X3), X5)
DB_IN_GGA(div(X1, X2), div(X1, X2), 0) → U28_GGA(X1, X2, isnumberA_in_g(times(X1, power(X2, p(0)))))
DB_IN_GGA(div(X1, X2), div(X1, X2), 0) → ISNUMBERA_IN_G(times(X1, power(X2, p(0))))
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U29_GGA(X1, X2, X3, X4, dB_in_gga(X1, div(X1, X2), X4))
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → DB_IN_GGA(X1, div(X1, X2), X4)
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U30_GGA(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
U30_GGA(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U31_GGA(X1, X2, X3, X4, dB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U30_GGA(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → DB_IN_GGA(power(X2, p(0)), div(X1, X2), X3)
DB_IN_GGA(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U32_GGA(X1, X2, dB_in_gga(X1, power(X1, 0), X2))
DB_IN_GGA(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → DB_IN_GGA(X1, power(X1, 0), X2)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U33_GGA(X1, X2, X3, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U34_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U34_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U35_GGA(X1, X2, X3, dB_in_gga(X1, power(X1, s(X2)), X3))
U34_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)), X3)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U36_GGA(X1, X2, X3, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U37_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U37_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U38_GGA(X1, X2, X3, dB_in_gga(X1, power(X1, p(X2)), X3))
U37_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)), X3)
DB_IN_GGA(s(X1), X2, 0) → U39_GGA(X1, X2, isnumberA_in_g(X1))
DB_IN_GGA(s(X1), X2, 0) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(p(X1), X2, 0) → U40_GGA(X1, X2, isnumberA_in_g(X1))
DB_IN_GGA(p(X1), X2, 0) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U41_GGA(X1, X2, X3, X4, X5, dB_in_gga(X1, X3, X5))
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U42_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U42_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U43_GGA(X1, X2, X3, X4, X5, dB_in_gga(X2, X3, X4))
U42_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(div(X1, X2), X3, X4) → U44_GGA(X1, X2, X3, X4, dB_in_gga(times(X1, power(X2, p(0))), X3, X4))
DB_IN_GGA(div(X1, X2), X3, X4) → DB_IN_GGA(times(X1, power(X2, p(0))), X3, X4)
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U45_GGA(X1, X2, X3, X4, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U46_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U47_GGA(X1, X2, X3, X4, dB_in_gga(X1, X3, X4))
U46_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U48_GGA(X1, X2, X3, dB_in_gga(X2, X1, X3))
DB_IN_GGA(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → DB_IN_GGA(X2, X1, X3)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U49_GGA(X1, X2, X3, X4, isnumberA_in_g(X1))
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U50_GGA(X1, X2, X3, X4, isnumbercA_in_g(X1))
U50_GGA(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U51_GGA(X1, X2, X3, X4, dB_in_gga(X2, X3, X4))
U50_GGA(X1, X2, X3, X4, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U52_GGA(X1, X2, X3, X4, X5, X6, X7, dB_in_gga(X1, X4, X7))
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → DB_IN_GGA(X1, X4, X7)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U54_GGA(X1, X2, X3, X4, X5, X6, X7, dB_in_gga(X2, X4, X6))
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → DB_IN_GGA(X2, X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U57_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(times(X1, power(X2, p(0))), X4, X6))
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U58_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
U58_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U59_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X3, X4, X5))
U58_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → DB_IN_GGA(X3, X4, X5)
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U60_GGA(X1, X2, X3, X4, X5, X6, isnumberA_in_g(X2))
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U62_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X1, X4, X6))
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X4, X6)
DB_IN_GGA(div(X1, X2), X3, 0) → U65_GGA(X1, X2, X3, isnumberA_in_g(times(X1, power(X2, p(0)))))
DB_IN_GGA(div(X1, X2), X3, 0) → ISNUMBERA_IN_G(times(X1, power(X2, p(0))))
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U66_GGA(X1, X2, X3, X4, X5, dB_in_gga(X1, X3, X5))
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U67_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U67_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U68_GGA(X1, X2, X3, X4, X5, dB_in_gga(power(X2, p(0)), X3, X4))
U67_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(power(X2, p(0)), X3, X4)
DB_IN_GGA(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U69_GGA(X1, X2, X3, dB_in_gga(X1, X2, X3))
DB_IN_GGA(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → DB_IN_GGA(X1, X2, X3)
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U70_GGA(X1, X2, X3, X4, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U71_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U72_GGA(X1, X2, X3, X4, dB_in_gga(X1, X3, X4))
U71_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U73_GGA(X1, X2, X3, X4, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U74_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U75_GGA(X1, X2, X3, X4, dB_in_gga(X1, X3, X4))
U74_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U63_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
U63_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U64_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X3, X4, X5))
U63_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U56_GGA(X1, X2, X3, X4, X5, X6, X7, dB_in_gga(X3, X4, X5))
U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U26_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
U26_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U27_GGA(X1, X2, X3, X4, X5, dB_in_gga(X3, times(power(X1, X2), X3), X4))
U26_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(power(X1, X2), X3), X4)
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U18_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U18_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U19_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X3, times(times(X1, X2), X3), X4))
U18_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(times(X1, X2), X3), X4)
dcB_in_gga(X1, X1, 1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(0, 0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1), 0) → U79_gga(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
dcB_in_gga(p(X1), p(X1), 0) → U80_gga(X1, isnumbercA_in_g(X1))
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U81_gga(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
dcB_in_gga(div(X1, X2), div(X1, X2), X3) → U83_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
dcB_in_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U84_gga(X1, X2, X3, isnumbercA_in_g(X2))
U84_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U85_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, X2), X3))
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U86_gga(X1, X2, X3, isnumbercA_in_g(X1))
U86_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U87_gga(X1, X2, X3, dcB_in_gga(X2, times(X1, X2), X3))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U88_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U91_gga(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U93_gga(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U93_gga(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
dcB_in_gga(div(X1, X2), div(X1, X2), 0) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U96_gga(X1, X2, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), div(X1, X2), 0)
dcB_in_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U97_gga(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
dcB_in_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U99_gga(X1, X2, dcB_in_gga(X1, power(X1, 0), X2))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U100_gga(X1, X2, X3, isnumbercA_in_g(X2))
U100_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U101_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, s(X2)), X3))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U102_gga(X1, X2, X3, isnumbercA_in_g(X2))
U102_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U103_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, p(X2)), X3))
dcB_in_gga(0, X1, 0) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2, 0) → U104_gga(X1, X2, isnumbercA_in_g(X1))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
dcB_in_gga(p(X1), X2, 0) → U105_gga(X1, X2, isnumbercA_in_g(X1))
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U106_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(div(X1, X2), X3, X4) → U108_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X3, X4))
dcB_in_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U109_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U109_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U111_gga(X1, X2, X3, dcB_in_gga(X2, X1, X3))
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U112_gga(X1, X2, X3, X4, isnumbercA_in_g(X1))
U112_gga(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, X4, dcB_in_gga(X2, X3, X4))
dcB_in_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
dcB_in_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U117_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
dcB_in_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0))), 1) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3, 0) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U122_gga(X1, X2, X3, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), X3, 0)
dcB_in_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U123_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U125_gga(X1, X2, X3, dcB_in_gga(X1, X2, X3))
dcB_in_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U126_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U126_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U128_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U128_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U129_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U127_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U125_gga(X1, X2, X3, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U123_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X4, X5, dcB_in_gga(power(X2, p(0)), X3, X4))
U124_gga(X1, X2, X3, X4, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U120_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U121_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
U117_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U118_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X3, X4, X5))
U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U113_gga(X1, X2, X3, X4, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U111_gga(X1, X2, X3, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U110_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U108_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U106_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X4, X5, dcB_in_gga(X2, X3, X4))
U107_gga(X1, X2, X3, X4, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U103_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U101_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U99_gga(X1, X2, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U97_gga(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X3, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U98_gga(X1, X2, X3, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U94_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(power(X1, X2), X3), X4))
U95_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U91_gga(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(div(X1, X2), X3), X4))
U92_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U88_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U89_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3), X4))
U90_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U87_gga(X1, X2, X3, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U85_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U83_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U81_gga(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X3, X4, dcB_in_gga(X2, times(X1, X2), X3))
U82_gga(X1, X2, X3, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
DB_IN_GGA(s(X1), s(X1), 0) → U3_GGA(X1, isnumberA_in_g(X1))
DB_IN_GGA(s(X1), s(X1), 0) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(s(X1)) → U1_G(X1, isnumberA_in_g(X1))
ISNUMBERA_IN_G(s(X1)) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(p(X1)) → U2_G(X1, isnumberA_in_g(X1))
ISNUMBERA_IN_G(p(X1)) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(p(X1), p(X1), 0) → U4_GGA(X1, isnumberA_in_g(X1))
DB_IN_GGA(p(X1), p(X1), 0) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U5_GGA(X1, X2, X3, X4, dB_in_gga(X1, times(X1, X2), X4))
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → DB_IN_GGA(X1, times(X1, X2), X4)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U6_GGA(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
U6_GGA(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U7_GGA(X1, X2, X3, X4, dB_in_gga(X2, times(X1, X2), X3))
U6_GGA(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(div(X1, X2), div(X1, X2), X3) → U8_GGA(X1, X2, X3, dB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
DB_IN_GGA(div(X1, X2), div(X1, X2), X3) → DB_IN_GGA(times(X1, power(X2, p(0))), div(X1, X2), X3)
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U9_GGA(X1, X2, X3, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U10_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U10_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U11_GGA(X1, X2, X3, dB_in_gga(X1, power(X1, X2), X3))
U10_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2), X3)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U12_GGA(X1, X2, X3, isnumberA_in_g(X1))
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U13_GGA(X1, X2, X3, isnumbercA_in_g(X1))
U13_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → U14_GGA(X1, X2, X3, dB_in_gga(X2, times(X1, X2), X3))
U13_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U15_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X1, times(times(X1, X2), X3), X6))
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → DB_IN_GGA(X1, times(times(X1, X2), X3), X6)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U16_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U17_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X2, times(times(X1, X2), X3), X5))
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → DB_IN_GGA(X2, times(times(X1, X2), X3), X5)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U20_GGA(X1, X2, X3, X4, X5, dB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U21_GGA(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
U21_GGA(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U22_GGA(X1, X2, X3, X4, X5, dB_in_gga(X3, times(div(X1, X2), X3), X4))
U21_GGA(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(div(X1, X2), X3), X4)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U23_GGA(X1, X2, X3, X4, X5, isnumberA_in_g(X2))
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U24_GGA(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U25_GGA(X1, X2, X3, X4, X5, dB_in_gga(X1, times(power(X1, X2), X3), X5))
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, times(power(X1, X2), X3), X5)
DB_IN_GGA(div(X1, X2), div(X1, X2), 0) → U28_GGA(X1, X2, isnumberA_in_g(times(X1, power(X2, p(0)))))
DB_IN_GGA(div(X1, X2), div(X1, X2), 0) → ISNUMBERA_IN_G(times(X1, power(X2, p(0))))
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U29_GGA(X1, X2, X3, X4, dB_in_gga(X1, div(X1, X2), X4))
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → DB_IN_GGA(X1, div(X1, X2), X4)
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U30_GGA(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
U30_GGA(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U31_GGA(X1, X2, X3, X4, dB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U30_GGA(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → DB_IN_GGA(power(X2, p(0)), div(X1, X2), X3)
DB_IN_GGA(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U32_GGA(X1, X2, dB_in_gga(X1, power(X1, 0), X2))
DB_IN_GGA(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → DB_IN_GGA(X1, power(X1, 0), X2)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U33_GGA(X1, X2, X3, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U34_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U34_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U35_GGA(X1, X2, X3, dB_in_gga(X1, power(X1, s(X2)), X3))
U34_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)), X3)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U36_GGA(X1, X2, X3, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U37_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U37_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U38_GGA(X1, X2, X3, dB_in_gga(X1, power(X1, p(X2)), X3))
U37_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)), X3)
DB_IN_GGA(s(X1), X2, 0) → U39_GGA(X1, X2, isnumberA_in_g(X1))
DB_IN_GGA(s(X1), X2, 0) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(p(X1), X2, 0) → U40_GGA(X1, X2, isnumberA_in_g(X1))
DB_IN_GGA(p(X1), X2, 0) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U41_GGA(X1, X2, X3, X4, X5, dB_in_gga(X1, X3, X5))
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U42_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U42_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U43_GGA(X1, X2, X3, X4, X5, dB_in_gga(X2, X3, X4))
U42_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(div(X1, X2), X3, X4) → U44_GGA(X1, X2, X3, X4, dB_in_gga(times(X1, power(X2, p(0))), X3, X4))
DB_IN_GGA(div(X1, X2), X3, X4) → DB_IN_GGA(times(X1, power(X2, p(0))), X3, X4)
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U45_GGA(X1, X2, X3, X4, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U46_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U47_GGA(X1, X2, X3, X4, dB_in_gga(X1, X3, X4))
U46_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U48_GGA(X1, X2, X3, dB_in_gga(X2, X1, X3))
DB_IN_GGA(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → DB_IN_GGA(X2, X1, X3)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U49_GGA(X1, X2, X3, X4, isnumberA_in_g(X1))
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → ISNUMBERA_IN_G(X1)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U50_GGA(X1, X2, X3, X4, isnumbercA_in_g(X1))
U50_GGA(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U51_GGA(X1, X2, X3, X4, dB_in_gga(X2, X3, X4))
U50_GGA(X1, X2, X3, X4, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U52_GGA(X1, X2, X3, X4, X5, X6, X7, dB_in_gga(X1, X4, X7))
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → DB_IN_GGA(X1, X4, X7)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U54_GGA(X1, X2, X3, X4, X5, X6, X7, dB_in_gga(X2, X4, X6))
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → DB_IN_GGA(X2, X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U57_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(times(X1, power(X2, p(0))), X4, X6))
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U58_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
U58_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U59_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X3, X4, X5))
U58_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → DB_IN_GGA(X3, X4, X5)
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U60_GGA(X1, X2, X3, X4, X5, X6, isnumberA_in_g(X2))
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U62_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X1, X4, X6))
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X4, X6)
DB_IN_GGA(div(X1, X2), X3, 0) → U65_GGA(X1, X2, X3, isnumberA_in_g(times(X1, power(X2, p(0)))))
DB_IN_GGA(div(X1, X2), X3, 0) → ISNUMBERA_IN_G(times(X1, power(X2, p(0))))
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U66_GGA(X1, X2, X3, X4, X5, dB_in_gga(X1, X3, X5))
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U67_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U67_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U68_GGA(X1, X2, X3, X4, X5, dB_in_gga(power(X2, p(0)), X3, X4))
U67_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(power(X2, p(0)), X3, X4)
DB_IN_GGA(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U69_GGA(X1, X2, X3, dB_in_gga(X1, X2, X3))
DB_IN_GGA(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → DB_IN_GGA(X1, X2, X3)
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U70_GGA(X1, X2, X3, X4, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U71_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U72_GGA(X1, X2, X3, X4, dB_in_gga(X1, X3, X4))
U71_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U73_GGA(X1, X2, X3, X4, isnumberA_in_g(X2))
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → ISNUMBERA_IN_G(X2)
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U74_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U75_GGA(X1, X2, X3, X4, dB_in_gga(X1, X3, X4))
U74_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U63_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
U63_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U64_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X3, X4, X5))
U63_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U56_GGA(X1, X2, X3, X4, X5, X6, X7, dB_in_gga(X3, X4, X5))
U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U26_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
U26_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U27_GGA(X1, X2, X3, X4, X5, dB_in_gga(X3, times(power(X1, X2), X3), X4))
U26_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(power(X1, X2), X3), X4)
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U18_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U18_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U19_GGA(X1, X2, X3, X4, X5, X6, dB_in_gga(X3, times(times(X1, X2), X3), X4))
U18_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(times(X1, X2), X3), X4)
dcB_in_gga(X1, X1, 1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(0, 0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1), 0) → U79_gga(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
dcB_in_gga(p(X1), p(X1), 0) → U80_gga(X1, isnumbercA_in_g(X1))
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U81_gga(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
dcB_in_gga(div(X1, X2), div(X1, X2), X3) → U83_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
dcB_in_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U84_gga(X1, X2, X3, isnumbercA_in_g(X2))
U84_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U85_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, X2), X3))
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U86_gga(X1, X2, X3, isnumbercA_in_g(X1))
U86_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U87_gga(X1, X2, X3, dcB_in_gga(X2, times(X1, X2), X3))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U88_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U91_gga(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U93_gga(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U93_gga(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
dcB_in_gga(div(X1, X2), div(X1, X2), 0) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U96_gga(X1, X2, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), div(X1, X2), 0)
dcB_in_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U97_gga(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
dcB_in_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U99_gga(X1, X2, dcB_in_gga(X1, power(X1, 0), X2))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U100_gga(X1, X2, X3, isnumbercA_in_g(X2))
U100_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U101_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, s(X2)), X3))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U102_gga(X1, X2, X3, isnumbercA_in_g(X2))
U102_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U103_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, p(X2)), X3))
dcB_in_gga(0, X1, 0) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2, 0) → U104_gga(X1, X2, isnumbercA_in_g(X1))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
dcB_in_gga(p(X1), X2, 0) → U105_gga(X1, X2, isnumbercA_in_g(X1))
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U106_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(div(X1, X2), X3, X4) → U108_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X3, X4))
dcB_in_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U109_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U109_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U111_gga(X1, X2, X3, dcB_in_gga(X2, X1, X3))
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U112_gga(X1, X2, X3, X4, isnumbercA_in_g(X1))
U112_gga(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, X4, dcB_in_gga(X2, X3, X4))
dcB_in_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
dcB_in_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U117_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
dcB_in_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0))), 1) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3, 0) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U122_gga(X1, X2, X3, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), X3, 0)
dcB_in_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U123_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U125_gga(X1, X2, X3, dcB_in_gga(X1, X2, X3))
dcB_in_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U126_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U126_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U128_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U128_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U129_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U127_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U125_gga(X1, X2, X3, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U123_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X4, X5, dcB_in_gga(power(X2, p(0)), X3, X4))
U124_gga(X1, X2, X3, X4, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U120_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U121_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
U117_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U118_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X3, X4, X5))
U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U113_gga(X1, X2, X3, X4, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U111_gga(X1, X2, X3, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U110_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U108_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U106_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X4, X5, dcB_in_gga(X2, X3, X4))
U107_gga(X1, X2, X3, X4, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U103_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U101_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U99_gga(X1, X2, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U97_gga(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X3, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U98_gga(X1, X2, X3, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U94_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(power(X1, X2), X3), X4))
U95_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U91_gga(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(div(X1, X2), X3), X4))
U92_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U88_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U89_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3), X4))
U90_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U87_gga(X1, X2, X3, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U85_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U83_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U81_gga(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X3, X4, dcB_in_gga(X2, times(X1, X2), X3))
U82_gga(X1, X2, X3, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
ISNUMBERA_IN_G(p(X1)) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(s(X1)) → ISNUMBERA_IN_G(X1)
dcB_in_gga(X1, X1, 1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(0, 0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1), 0) → U79_gga(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
dcB_in_gga(p(X1), p(X1), 0) → U80_gga(X1, isnumbercA_in_g(X1))
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U81_gga(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
dcB_in_gga(div(X1, X2), div(X1, X2), X3) → U83_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
dcB_in_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U84_gga(X1, X2, X3, isnumbercA_in_g(X2))
U84_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U85_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, X2), X3))
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U86_gga(X1, X2, X3, isnumbercA_in_g(X1))
U86_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U87_gga(X1, X2, X3, dcB_in_gga(X2, times(X1, X2), X3))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U88_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U91_gga(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U93_gga(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U93_gga(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
dcB_in_gga(div(X1, X2), div(X1, X2), 0) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U96_gga(X1, X2, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), div(X1, X2), 0)
dcB_in_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U97_gga(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
dcB_in_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U99_gga(X1, X2, dcB_in_gga(X1, power(X1, 0), X2))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U100_gga(X1, X2, X3, isnumbercA_in_g(X2))
U100_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U101_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, s(X2)), X3))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U102_gga(X1, X2, X3, isnumbercA_in_g(X2))
U102_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U103_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, p(X2)), X3))
dcB_in_gga(0, X1, 0) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2, 0) → U104_gga(X1, X2, isnumbercA_in_g(X1))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
dcB_in_gga(p(X1), X2, 0) → U105_gga(X1, X2, isnumbercA_in_g(X1))
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U106_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(div(X1, X2), X3, X4) → U108_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X3, X4))
dcB_in_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U109_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U109_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U111_gga(X1, X2, X3, dcB_in_gga(X2, X1, X3))
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U112_gga(X1, X2, X3, X4, isnumbercA_in_g(X1))
U112_gga(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, X4, dcB_in_gga(X2, X3, X4))
dcB_in_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
dcB_in_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U117_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
dcB_in_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0))), 1) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3, 0) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U122_gga(X1, X2, X3, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), X3, 0)
dcB_in_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U123_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U125_gga(X1, X2, X3, dcB_in_gga(X1, X2, X3))
dcB_in_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U126_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U126_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U128_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U128_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U129_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U127_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U125_gga(X1, X2, X3, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U123_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X4, X5, dcB_in_gga(power(X2, p(0)), X3, X4))
U124_gga(X1, X2, X3, X4, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U120_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U121_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
U117_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U118_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X3, X4, X5))
U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U113_gga(X1, X2, X3, X4, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U111_gga(X1, X2, X3, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U110_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U108_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U106_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X4, X5, dcB_in_gga(X2, X3, X4))
U107_gga(X1, X2, X3, X4, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U103_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U101_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U99_gga(X1, X2, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U97_gga(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X3, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U98_gga(X1, X2, X3, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U94_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(power(X1, X2), X3), X4))
U95_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U91_gga(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(div(X1, X2), X3), X4))
U92_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U88_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U89_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3), X4))
U90_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U87_gga(X1, X2, X3, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U85_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U83_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U81_gga(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X3, X4, dcB_in_gga(X2, times(X1, X2), X3))
U82_gga(X1, X2, X3, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
ISNUMBERA_IN_G(p(X1)) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(s(X1)) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(p(X1)) → ISNUMBERA_IN_G(X1)
ISNUMBERA_IN_G(s(X1)) → ISNUMBERA_IN_G(X1)
From the DPs we obtained the following set of size-change graphs:
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → DB_IN_GGA(X1, times(X1, X2), X4)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U6_GGA(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
U6_GGA(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U13_GGA(X1, X2, X3, isnumbercA_in_g(X1))
U13_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → DB_IN_GGA(X1, times(times(X1, X2), X3), X6)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U16_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → DB_IN_GGA(X2, times(times(X1, X2), X3), X5)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(div(X1, X2), div(X1, X2), X3) → DB_IN_GGA(times(X1, power(X2, p(0))), div(X1, X2), X3)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U42_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U42_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U10_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U10_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2), X3)
DB_IN_GGA(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → DB_IN_GGA(X1, power(X1, 0), X2)
DB_IN_GGA(div(X1, X2), X3, X4) → DB_IN_GGA(times(X1, power(X2, p(0))), X3, X4)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U21_GGA(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
U21_GGA(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(div(X1, X2), X3), X4)
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U46_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U24_GGA(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, times(power(X1, X2), X3), X5)
DB_IN_GGA(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → DB_IN_GGA(X2, X1, X3)
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → DB_IN_GGA(X1, div(X1, X2), X4)
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U30_GGA(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
U30_GGA(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → DB_IN_GGA(power(X2, p(0)), div(X1, X2), X3)
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U74_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U34_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U34_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)), X3)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U50_GGA(X1, X2, X3, X4, isnumbercA_in_g(X1))
U50_GGA(X1, X2, X3, X4, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U37_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U37_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)), X3)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → DB_IN_GGA(X1, X4, X7)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → DB_IN_GGA(X2, X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U58_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
U58_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → DB_IN_GGA(X3, X4, X5)
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X4, X6)
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U67_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U67_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(power(X2, p(0)), X3, X4)
DB_IN_GGA(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → DB_IN_GGA(X1, X2, X3)
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U71_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U63_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
U63_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U26_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
U26_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(power(X1, X2), X3), X4)
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U18_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U18_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(times(X1, X2), X3), X4)
dcB_in_gga(X1, X1, 1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(0, 0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1), 0) → U79_gga(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
dcB_in_gga(p(X1), p(X1), 0) → U80_gga(X1, isnumbercA_in_g(X1))
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U81_gga(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
dcB_in_gga(div(X1, X2), div(X1, X2), X3) → U83_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
dcB_in_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U84_gga(X1, X2, X3, isnumbercA_in_g(X2))
U84_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U85_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, X2), X3))
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U86_gga(X1, X2, X3, isnumbercA_in_g(X1))
U86_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U87_gga(X1, X2, X3, dcB_in_gga(X2, times(X1, X2), X3))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U88_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U91_gga(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U93_gga(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U93_gga(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
dcB_in_gga(div(X1, X2), div(X1, X2), 0) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U96_gga(X1, X2, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), div(X1, X2), 0)
dcB_in_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U97_gga(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
dcB_in_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U99_gga(X1, X2, dcB_in_gga(X1, power(X1, 0), X2))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U100_gga(X1, X2, X3, isnumbercA_in_g(X2))
U100_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U101_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, s(X2)), X3))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U102_gga(X1, X2, X3, isnumbercA_in_g(X2))
U102_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U103_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, p(X2)), X3))
dcB_in_gga(0, X1, 0) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2, 0) → U104_gga(X1, X2, isnumbercA_in_g(X1))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
dcB_in_gga(p(X1), X2, 0) → U105_gga(X1, X2, isnumbercA_in_g(X1))
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U106_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(div(X1, X2), X3, X4) → U108_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X3, X4))
dcB_in_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U109_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U109_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U111_gga(X1, X2, X3, dcB_in_gga(X2, X1, X3))
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U112_gga(X1, X2, X3, X4, isnumbercA_in_g(X1))
U112_gga(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, X4, dcB_in_gga(X2, X3, X4))
dcB_in_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
dcB_in_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U117_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
dcB_in_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0))), 1) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3, 0) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
U122_gga(X1, X2, X3, isnumbercA_out_g(times(X1, power(X2, p(0))))) → dcB_out_gga(div(X1, X2), X3, 0)
dcB_in_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U123_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U125_gga(X1, X2, X3, dcB_in_gga(X1, X2, X3))
dcB_in_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U126_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U126_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
dcB_in_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U128_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
U128_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U129_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U127_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U125_gga(X1, X2, X3, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U123_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X4, X5, dcB_in_gga(power(X2, p(0)), X3, X4))
U124_gga(X1, X2, X3, X4, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U120_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U121_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
U117_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U118_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X3, X4, X5))
U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U113_gga(X1, X2, X3, X4, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U111_gga(X1, X2, X3, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U110_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U108_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U106_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X4, X5, dcB_in_gga(X2, X3, X4))
U107_gga(X1, X2, X3, X4, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U103_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U101_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U99_gga(X1, X2, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U97_gga(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X3, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U98_gga(X1, X2, X3, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U94_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(power(X1, X2), X3), X4))
U95_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U91_gga(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(div(X1, X2), X3), X4))
U92_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U88_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U89_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3), X4))
U90_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U87_gga(X1, X2, X3, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U85_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U83_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U81_gga(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X3, X4, dcB_in_gga(X2, times(X1, X2), X3))
U82_gga(X1, X2, X3, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → DB_IN_GGA(X1, times(X1, X2), X4)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U6_GGA(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
U6_GGA(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U13_GGA(X1, X2, X3, isnumbercA_in_g(X1))
U13_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, times(X1, X2), X3)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → DB_IN_GGA(X1, times(times(X1, X2), X3), X6)
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U16_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → DB_IN_GGA(X2, times(times(X1, X2), X3), X5)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(div(X1, X2), div(X1, X2), X3) → DB_IN_GGA(times(X1, power(X2, p(0))), div(X1, X2), X3)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U42_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U42_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U10_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U10_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2), X3)
DB_IN_GGA(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → DB_IN_GGA(X1, power(X1, 0), X2)
DB_IN_GGA(div(X1, X2), X3, X4) → DB_IN_GGA(times(X1, power(X2, p(0))), X3, X4)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U21_GGA(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
U21_GGA(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(div(X1, X2), X3), X4)
DB_IN_GGA(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U46_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U24_GGA(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, times(power(X1, X2), X3), X5)
DB_IN_GGA(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → DB_IN_GGA(X2, X1, X3)
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → DB_IN_GGA(X1, div(X1, X2), X4)
DB_IN_GGA(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U30_GGA(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
U30_GGA(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → DB_IN_GGA(power(X2, p(0)), div(X1, X2), X3)
DB_IN_GGA(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U74_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U34_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U34_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)), X3)
DB_IN_GGA(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U50_GGA(X1, X2, X3, X4, isnumbercA_in_g(X1))
U50_GGA(X1, X2, X3, X4, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, X3, X4)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U37_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U37_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)), X3)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → DB_IN_GGA(X1, X4, X7)
DB_IN_GGA(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → DB_IN_GGA(X2, X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → DB_IN_GGA(times(X1, power(X2, p(0))), X4, X6)
DB_IN_GGA(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U58_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
U58_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → DB_IN_GGA(X3, X4, X5)
DB_IN_GGA(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X4, X6)
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → DB_IN_GGA(X1, X3, X5)
DB_IN_GGA(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U67_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
U67_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(power(X2, p(0)), X3, X4)
DB_IN_GGA(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → DB_IN_GGA(X1, X2, X3)
DB_IN_GGA(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U71_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3, X4)
U61_GGA(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U63_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
U63_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U53_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U55_GGA(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → DB_IN_GGA(X3, X4, X5)
U24_GGA(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U26_GGA(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
U26_GGA(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(power(X1, X2), X3), X4)
U16_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U18_GGA(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U18_GGA(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(times(X1, X2), X3), X4)
dcB_in_gga(X1, X1, 1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2))) → U81_gga(X1, X2, X3, X4, dcB_in_gga(X1, times(X1, X2), X4))
dcB_in_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2))) → U86_gga(X1, X2, X3, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3))) → U88_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, times(times(X1, X2), X3), X6))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3))) → U91_gga(X1, X2, X3, X4, X5, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3))) → U93_gga(X1, X2, X3, X4, X5, isnumbercA_in_g(X2))
dcB_in_gga(0, X1, 0) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2, 0) → U104_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), X2, 0) → U105_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2))) → U106_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(div(X1, X2), X3, X4) → U108_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X3, X4))
dcB_in_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2))))) → U109_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
dcB_in_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2))) → U111_gga(X1, X2, X3, dcB_in_gga(X2, X1, X3))
dcB_in_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2))) → U112_gga(X1, X2, X3, X4, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3))) → U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X1, X4, X7))
dcB_in_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3))) → U117_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(times(X1, power(X2, p(0))), X4, X6))
dcB_in_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3))) → U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0))), 1) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3, 0) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0))))) → U123_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, X3, X5))
dcB_in_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0))))) → U125_gga(X1, X2, X3, dcB_in_gga(X1, X2, X3))
dcB_in_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2)))))) → U126_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2)))))) → U128_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
dcB_in_gga(0, 0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1), 0) → U79_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), p(X1), 0) → U80_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(div(X1, X2), div(X1, X2), X3) → U83_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2), X3))
dcB_in_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2))))) → U84_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), div(X1, X2), 0) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0))))) → U97_gga(X1, X2, X3, X4, dcB_in_gga(X1, div(X1, X2), X4))
dcB_in_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0))))) → U99_gga(X1, X2, dcB_in_gga(X1, power(X1, 0), X2))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2)))))) → U100_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2)))))) → U102_gga(X1, X2, X3, isnumbercA_in_g(X2))
U81_gga(X1, X2, X3, X4, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X3, X4, dcB_in_gga(X2, times(X1, X2), X3))
U86_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U87_gga(X1, X2, X3, dcB_in_gga(X2, times(X1, X2), X3))
U88_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X2, times(times(X1, X2), X3), X5))
U91_gga(X1, X2, X3, X4, X5, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(div(X1, X2), X3), X4))
U93_gga(X1, X2, X3, X4, X5, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, X4, X5, dcB_in_gga(X1, times(power(X1, X2), X3), X5))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
U106_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X4, X5, dcB_in_gga(X2, X3, X4))
U108_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U109_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U111_gga(X1, X2, X3, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U112_gga(X1, X2, X3, X4, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, X4, dcB_in_gga(X2, X3, X4))
U114_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X2, X4, X6))
U117_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U119_gga(X1, X2, X3, X4, X5, X6, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X1, X4, X6))
U123_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X4, X5, dcB_in_gga(power(X2, p(0)), X3, X4))
U125_gga(X1, X2, X3, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U126_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U128_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, X4, dcB_in_gga(X1, X3, X4))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
U83_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U84_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U85_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, X2), X3))
U97_gga(X1, X2, X3, X4, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X3, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2), X3))
U99_gga(X1, X2, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U100_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U101_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, s(X2)), X3))
U102_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U103_gga(X1, X2, X3, dcB_in_gga(X1, power(X1, p(X2)), X3))
U82_gga(X1, X2, X3, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
U87_gga(X1, X2, X3, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U89_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3), X4))
U92_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U94_gga(X1, X2, X3, X4, X5, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X4, X5, dcB_in_gga(X3, times(power(X1, X2), X3), X4))
U107_gga(X1, X2, X3, X4, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U110_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U113_gga(X1, X2, X3, X4, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U115_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_in_gga(X3, X4, X5))
U118_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U120_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X5, X6, dcB_in_gga(X3, X4, X5))
U124_gga(X1, X2, X3, X4, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U127_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U129_gga(X1, X2, X3, X4, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U85_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U98_gga(X1, X2, X3, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U101_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U103_gga(X1, X2, X3, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U90_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U95_gga(X1, X2, X3, X4, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U116_gga(X1, X2, X3, X4, X5, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U121_gga(X1, X2, X3, X4, X5, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
DB_IN_GGA(times(X1, X2), times(X1, X2)) → DB_IN_GGA(X1, times(X1, X2))
DB_IN_GGA(times(X1, X2), times(X1, X2)) → U6_GGA(X1, X2, dcB_in_gga(X1, times(X1, X2)))
U6_GGA(X1, X2, dcB_out_gga(X1, times(X1, X2), X4)) → DB_IN_GGA(X2, times(X1, X2))
DB_IN_GGA(times(X1, X2), times(X1, X2)) → U13_GGA(X1, X2, isnumbercA_in_g(X1))
U13_GGA(X1, X2, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, times(X1, X2))
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3)) → DB_IN_GGA(X1, times(times(X1, X2), X3))
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3)) → U16_GGA(X1, X2, X3, dcB_in_gga(X1, times(times(X1, X2), X3)))
U16_GGA(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → DB_IN_GGA(X2, times(times(X1, X2), X3))
DB_IN_GGA(times(X1, X2), X3) → DB_IN_GGA(X1, X3)
DB_IN_GGA(div(X1, X2), div(X1, X2)) → DB_IN_GGA(times(X1, power(X2, p(0))), div(X1, X2))
DB_IN_GGA(times(X1, X2), X3) → U42_GGA(X1, X2, X3, dcB_in_gga(X1, X3))
U42_GGA(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(X2, X3)
DB_IN_GGA(power(X1, X2), power(X1, X2)) → U10_GGA(X1, X2, isnumbercA_in_g(X2))
U10_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2))
DB_IN_GGA(power(X1, 0), power(X1, 0)) → DB_IN_GGA(X1, power(X1, 0))
DB_IN_GGA(div(X1, X2), X3) → DB_IN_GGA(times(X1, power(X2, p(0))), X3)
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3)) → DB_IN_GGA(times(X1, power(X2, p(0))), times(div(X1, X2), X3))
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3)) → U21_GGA(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3)))
U21_GGA(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(div(X1, X2), X3))
DB_IN_GGA(power(X1, X2), X3) → U46_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3)) → U24_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U24_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, times(power(X1, X2), X3))
DB_IN_GGA(times(X1, X2), X1) → DB_IN_GGA(X2, X1)
DB_IN_GGA(div(X1, X2), div(X1, X2)) → DB_IN_GGA(X1, div(X1, X2))
DB_IN_GGA(div(X1, X2), div(X1, X2)) → U30_GGA(X1, X2, dcB_in_gga(X1, div(X1, X2)))
U30_GGA(X1, X2, dcB_out_gga(X1, div(X1, X2), X4)) → DB_IN_GGA(power(X2, p(0)), div(X1, X2))
DB_IN_GGA(power(X1, p(X2)), X3) → U74_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2))) → U34_GGA(X1, X2, isnumbercA_in_g(X2))
U34_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)))
DB_IN_GGA(times(X1, X2), X3) → U50_GGA(X1, X2, X3, isnumbercA_in_g(X1))
U50_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, X3)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2))) → U37_GGA(X1, X2, isnumbercA_in_g(X2))
U37_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)))
DB_IN_GGA(times(times(X1, X2), X3), X4) → DB_IN_GGA(X1, X4)
DB_IN_GGA(times(times(X1, X2), X3), X4) → U53_GGA(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U53_GGA(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → DB_IN_GGA(X2, X4)
DB_IN_GGA(times(div(X1, X2), X3), X4) → DB_IN_GGA(times(X1, power(X2, p(0))), X4)
DB_IN_GGA(times(div(X1, X2), X3), X4) → U58_GGA(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X4))
U58_GGA(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → DB_IN_GGA(X3, X4)
DB_IN_GGA(times(power(X1, X2), X3), X4) → U61_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
U61_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X4)
DB_IN_GGA(div(X1, X2), X3) → DB_IN_GGA(X1, X3)
DB_IN_GGA(div(X1, X2), X3) → U67_GGA(X1, X2, X3, dcB_in_gga(X1, X3))
U67_GGA(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(power(X2, p(0)), X3)
DB_IN_GGA(power(X1, 0), X2) → DB_IN_GGA(X1, X2)
DB_IN_GGA(power(X1, s(X2)), X3) → U71_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
U61_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U63_GGA(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U63_GGA(X1, X2, X3, X4, dcB_out_gga(X1, X4, X6)) → DB_IN_GGA(X3, X4)
U53_GGA(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → U55_GGA(X1, X2, X3, X4, dcB_in_gga(X2, X4))
U55_GGA(X1, X2, X3, X4, dcB_out_gga(X2, X4, X6)) → DB_IN_GGA(X3, X4)
U24_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U26_GGA(X1, X2, X3, dcB_in_gga(X1, times(power(X1, X2), X3)))
U26_GGA(X1, X2, X3, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(power(X1, X2), X3))
U16_GGA(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U18_GGA(X1, X2, X3, dcB_in_gga(X2, times(times(X1, X2), X3)))
U18_GGA(X1, X2, X3, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(times(X1, X2), X3))
dcB_in_gga(X1, X1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(times(X1, X2), times(X1, X2)) → U81_gga(X1, X2, dcB_in_gga(X1, times(X1, X2)))
dcB_in_gga(times(X1, X2), times(X1, X2)) → U86_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3)) → U88_gga(X1, X2, X3, dcB_in_gga(X1, times(times(X1, X2), X3)))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3)) → U91_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3)))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3)) → U93_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(0, X1) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2) → U104_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), X2) → U105_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(X1, X2), X3) → U106_gga(X1, X2, X3, dcB_in_gga(X1, X3))
dcB_in_gga(div(X1, X2), X3) → U108_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), X3))
dcB_in_gga(power(X1, X2), X3) → U109_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(times(X1, X2), X1) → U111_gga(X1, X2, dcB_in_gga(X2, X1))
dcB_in_gga(times(X1, X2), X3) → U112_gga(X1, X2, X3, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), X4) → U114_gga(X1, X2, X3, X4, dcB_in_gga(X1, X4))
dcB_in_gga(times(div(X1, X2), X3), X4) → U117_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X4))
dcB_in_gga(times(power(X1, X2), X3), X4) → U119_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0)))) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), X3) → U123_gga(X1, X2, X3, dcB_in_gga(X1, X3))
dcB_in_gga(power(X1, 0), X2) → U125_gga(X1, X2, dcB_in_gga(X1, X2))
dcB_in_gga(power(X1, s(X2)), X3) → U126_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), X3) → U128_gga(X1, X2, X3, isnumbercA_in_g(X2))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
dcB_in_gga(0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1)) → U79_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), p(X1)) → U80_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U83_gga(X1, X2, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2)))
dcB_in_gga(power(X1, X2), power(X1, X2)) → U84_gga(X1, X2, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U97_gga(X1, X2, dcB_in_gga(X1, div(X1, X2)))
dcB_in_gga(power(X1, 0), power(X1, 0)) → U99_gga(X1, dcB_in_gga(X1, power(X1, 0)))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2))) → U100_gga(X1, X2, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2))) → U102_gga(X1, X2, isnumbercA_in_g(X2))
U81_gga(X1, X2, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X4, dcB_in_gga(X2, times(X1, X2)))
U86_gga(X1, X2, isnumbercA_out_g(X1)) → U87_gga(X1, X2, dcB_in_gga(X2, times(X1, X2)))
U88_gga(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X6, dcB_in_gga(X2, times(times(X1, X2), X3)))
U91_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X5, dcB_in_gga(X3, times(div(X1, X2), X3)))
U93_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, dcB_in_gga(X1, times(power(X1, X2), X3)))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
U106_gga(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X5, dcB_in_gga(X2, X3))
U108_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U109_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U111_gga(X1, X2, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U112_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, dcB_in_gga(X2, X3))
U114_gga(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X7, dcB_in_gga(X2, X4))
U117_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X6, dcB_in_gga(X3, X4))
U119_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U123_gga(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X5, dcB_in_gga(power(X2, p(0)), X3))
U125_gga(X1, X2, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U126_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U128_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
U83_gga(X1, X2, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U84_gga(X1, X2, isnumbercA_out_g(X2)) → U85_gga(X1, X2, dcB_in_gga(X1, power(X1, X2)))
U97_gga(X1, X2, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2)))
U99_gga(X1, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U100_gga(X1, X2, isnumbercA_out_g(X2)) → U101_gga(X1, X2, dcB_in_gga(X1, power(X1, s(X2))))
U102_gga(X1, X2, isnumbercA_out_g(X2)) → U103_gga(X1, X2, dcB_in_gga(X1, power(X1, p(X2))))
U82_gga(X1, X2, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
U87_gga(X1, X2, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U89_gga(X1, X2, X3, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3)))
U92_gga(X1, X2, X3, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U94_gga(X1, X2, X3, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X5, dcB_in_gga(X3, times(power(X1, X2), X3)))
U107_gga(X1, X2, X3, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U110_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U113_gga(X1, X2, X3, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U115_gga(X1, X2, X3, X4, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X6, X7, dcB_in_gga(X3, X4))
U118_gga(X1, X2, X3, X4, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U120_gga(X1, X2, X3, X4, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X6, dcB_in_gga(X3, X4))
U124_gga(X1, X2, X3, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U127_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U129_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U85_gga(X1, X2, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U98_gga(X1, X2, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U101_gga(X1, X2, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U103_gga(X1, X2, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U90_gga(X1, X2, X3, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U95_gga(X1, X2, X3, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U116_gga(X1, X2, X3, X4, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U121_gga(X1, X2, X3, X4, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
dcB_in_gga(x0, x1)
isnumbercA_in_g(x0)
U81_gga(x0, x1, x2)
U86_gga(x0, x1, x2)
U88_gga(x0, x1, x2, x3)
U91_gga(x0, x1, x2, x3)
U93_gga(x0, x1, x2, x3)
U104_gga(x0, x1, x2)
U105_gga(x0, x1, x2)
U106_gga(x0, x1, x2, x3)
U108_gga(x0, x1, x2, x3)
U109_gga(x0, x1, x2, x3)
U111_gga(x0, x1, x2)
U112_gga(x0, x1, x2, x3)
U114_gga(x0, x1, x2, x3, x4)
U117_gga(x0, x1, x2, x3, x4)
U119_gga(x0, x1, x2, x3, x4)
U123_gga(x0, x1, x2, x3)
U125_gga(x0, x1, x2)
U126_gga(x0, x1, x2, x3)
U128_gga(x0, x1, x2, x3)
U77_g(x0, x1)
U78_g(x0, x1)
U79_gga(x0, x1)
U80_gga(x0, x1)
U83_gga(x0, x1, x2)
U84_gga(x0, x1, x2)
U97_gga(x0, x1, x2)
U99_gga(x0, x1)
U100_gga(x0, x1, x2)
U102_gga(x0, x1, x2)
U82_gga(x0, x1, x2, x3)
U87_gga(x0, x1, x2)
U89_gga(x0, x1, x2, x3, x4)
U92_gga(x0, x1, x2, x3, x4)
U94_gga(x0, x1, x2, x3)
U107_gga(x0, x1, x2, x3, x4)
U110_gga(x0, x1, x2, x3)
U113_gga(x0, x1, x2, x3)
U115_gga(x0, x1, x2, x3, x4, x5)
U118_gga(x0, x1, x2, x3, x4, x5)
U120_gga(x0, x1, x2, x3, x4)
U124_gga(x0, x1, x2, x3, x4)
U127_gga(x0, x1, x2, x3)
U129_gga(x0, x1, x2, x3)
U85_gga(x0, x1, x2)
U98_gga(x0, x1, x2, x3)
U101_gga(x0, x1, x2)
U103_gga(x0, x1, x2)
U90_gga(x0, x1, x2, x3, x4, x5)
U95_gga(x0, x1, x2, x3, x4)
U116_gga(x0, x1, x2, x3, x4, x5, x6)
U121_gga(x0, x1, x2, x3, x4, x5)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
DB_IN_GGA(times(X1, X2), times(X1, X2)) → DB_IN_GGA(X1, times(X1, X2))
DB_IN_GGA(times(X1, X2), times(X1, X2)) → U6_GGA(X1, X2, dcB_in_gga(X1, times(X1, X2)))
DB_IN_GGA(times(X1, X2), times(X1, X2)) → U13_GGA(X1, X2, isnumbercA_in_g(X1))
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3)) → DB_IN_GGA(X1, times(times(X1, X2), X3))
DB_IN_GGA(times(times(X1, X2), X3), times(times(X1, X2), X3)) → U16_GGA(X1, X2, X3, dcB_in_gga(X1, times(times(X1, X2), X3)))
U16_GGA(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → DB_IN_GGA(X2, times(times(X1, X2), X3))
DB_IN_GGA(times(X1, X2), X3) → DB_IN_GGA(X1, X3)
DB_IN_GGA(times(X1, X2), X3) → U42_GGA(X1, X2, X3, dcB_in_gga(X1, X3))
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3)) → DB_IN_GGA(times(X1, power(X2, p(0))), times(div(X1, X2), X3))
DB_IN_GGA(times(div(X1, X2), X3), times(div(X1, X2), X3)) → U21_GGA(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3)))
U24_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, times(power(X1, X2), X3))
DB_IN_GGA(times(X1, X2), X1) → DB_IN_GGA(X2, X1)
DB_IN_GGA(div(X1, X2), div(X1, X2)) → DB_IN_GGA(X1, div(X1, X2))
DB_IN_GGA(div(X1, X2), div(X1, X2)) → U30_GGA(X1, X2, dcB_in_gga(X1, div(X1, X2)))
DB_IN_GGA(times(X1, X2), X3) → U50_GGA(X1, X2, X3, isnumbercA_in_g(X1))
DB_IN_GGA(times(times(X1, X2), X3), X4) → DB_IN_GGA(X1, X4)
DB_IN_GGA(times(times(X1, X2), X3), X4) → U53_GGA(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U53_GGA(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → DB_IN_GGA(X2, X4)
DB_IN_GGA(times(div(X1, X2), X3), X4) → DB_IN_GGA(times(X1, power(X2, p(0))), X4)
DB_IN_GGA(times(div(X1, X2), X3), X4) → U58_GGA(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X4))
U58_GGA(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → DB_IN_GGA(X3, X4)
DB_IN_GGA(times(power(X1, X2), X3), X4) → U61_GGA(X1, X2, X3, X4, isnumbercA_in_g(X2))
DB_IN_GGA(div(X1, X2), X3) → DB_IN_GGA(X1, X3)
U67_GGA(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(power(X2, p(0)), X3)
U55_GGA(X1, X2, X3, X4, dcB_out_gga(X2, X4, X6)) → DB_IN_GGA(X3, X4)
U26_GGA(X1, X2, X3, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(power(X1, X2), X3))
U16_GGA(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U18_GGA(X1, X2, X3, dcB_in_gga(X2, times(times(X1, X2), X3)))
POL(+(x1, x2)) = 0
POL(0) = 0
POL(1) = 0
POL(DB_IN_GGA(x1, x2)) = x1
POL(U100_gga(x1, x2, x3)) = 0
POL(U101_gga(x1, x2, x3)) = 0
POL(U102_gga(x1, x2, x3)) = 0
POL(U103_gga(x1, x2, x3)) = 0
POL(U104_gga(x1, x2, x3)) = 0
POL(U105_gga(x1, x2, x3)) = 0
POL(U106_gga(x1, x2, x3, x4)) = 0
POL(U107_gga(x1, x2, x3, x4, x5)) = 0
POL(U108_gga(x1, x2, x3, x4)) = 0
POL(U109_gga(x1, x2, x3, x4)) = 0
POL(U10_GGA(x1, x2, x3)) = x1
POL(U110_gga(x1, x2, x3, x4)) = 0
POL(U111_gga(x1, x2, x3)) = 0
POL(U112_gga(x1, x2, x3, x4)) = 0
POL(U113_gga(x1, x2, x3, x4)) = 0
POL(U114_gga(x1, x2, x3, x4, x5)) = 0
POL(U115_gga(x1, x2, x3, x4, x5, x6)) = 0
POL(U116_gga(x1, x2, x3, x4, x5, x6, x7)) = 0
POL(U117_gga(x1, x2, x3, x4, x5)) = 0
POL(U118_gga(x1, x2, x3, x4, x5, x6)) = 0
POL(U119_gga(x1, x2, x3, x4, x5)) = 0
POL(U120_gga(x1, x2, x3, x4, x5)) = 0
POL(U121_gga(x1, x2, x3, x4, x5, x6)) = 0
POL(U122_gga(x1, x2, x3, x4)) = 0
POL(U123_gga(x1, x2, x3, x4)) = 0
POL(U124_gga(x1, x2, x3, x4, x5)) = 0
POL(U125_gga(x1, x2, x3)) = 0
POL(U126_gga(x1, x2, x3, x4)) = 0
POL(U127_gga(x1, x2, x3, x4)) = 0
POL(U128_gga(x1, x2, x3, x4)) = 0
POL(U129_gga(x1, x2, x3, x4)) = 0
POL(U13_GGA(x1, x2, x3)) = x1 + x2
POL(U16_GGA(x1, x2, x3, x4)) = 1 + x2 + x3
POL(U18_GGA(x1, x2, x3, x4)) = x2 + x3
POL(U21_GGA(x1, x2, x3, x4)) = x1 + x2 + x3
POL(U24_GGA(x1, x2, x3, x4)) = 1 + x1 + x3
POL(U26_GGA(x1, x2, x3, x4)) = 1 + x1 + x3
POL(U30_GGA(x1, x2, x3)) = x1 + x2
POL(U34_GGA(x1, x2, x3)) = x1
POL(U37_GGA(x1, x2, x3)) = x1
POL(U42_GGA(x1, x2, x3, x4)) = x2
POL(U46_GGA(x1, x2, x3, x4)) = x1
POL(U50_GGA(x1, x2, x3, x4)) = x2
POL(U53_GGA(x1, x2, x3, x4, x5)) = 1 + x1 + x2 + x3
POL(U55_GGA(x1, x2, x3, x4, x5)) = 1 + x3
POL(U58_GGA(x1, x2, x3, x4, x5)) = 1 + x3
POL(U61_GGA(x1, x2, x3, x4, x5)) = x1 + x3
POL(U63_GGA(x1, x2, x3, x4, x5)) = x3
POL(U67_GGA(x1, x2, x3, x4)) = 1 + x2
POL(U6_GGA(x1, x2, x3)) = x1 + x2
POL(U71_GGA(x1, x2, x3, x4)) = x1
POL(U74_GGA(x1, x2, x3, x4)) = x1
POL(U77_g(x1, x2)) = 0
POL(U78_g(x1, x2)) = 0
POL(U79_gga(x1, x2)) = 0
POL(U80_gga(x1, x2)) = 0
POL(U81_gga(x1, x2, x3)) = 0
POL(U82_gga(x1, x2, x3, x4)) = 0
POL(U83_gga(x1, x2, x3)) = 0
POL(U84_gga(x1, x2, x3)) = 0
POL(U85_gga(x1, x2, x3)) = 0
POL(U86_gga(x1, x2, x3)) = 0
POL(U87_gga(x1, x2, x3)) = 0
POL(U88_gga(x1, x2, x3, x4)) = 0
POL(U89_gga(x1, x2, x3, x4, x5)) = 0
POL(U90_gga(x1, x2, x3, x4, x5, x6)) = 0
POL(U91_gga(x1, x2, x3, x4)) = 0
POL(U92_gga(x1, x2, x3, x4, x5)) = 0
POL(U93_gga(x1, x2, x3, x4)) = 0
POL(U94_gga(x1, x2, x3, x4)) = 0
POL(U95_gga(x1, x2, x3, x4, x5)) = 0
POL(U96_gga(x1, x2, x3)) = 0
POL(U97_gga(x1, x2, x3)) = 0
POL(U98_gga(x1, x2, x3, x4)) = 0
POL(U99_gga(x1, x2)) = 0
POL(dcB_in_gga(x1, x2)) = 0
POL(dcB_out_gga(x1, x2, x3)) = 0
POL(div(x1, x2)) = 1 + x1 + x2
POL(isnumbercA_in_g(x1)) = 0
POL(isnumbercA_out_g(x1)) = 0
POL(p(x1)) = 0
POL(power(x1, x2)) = x1
POL(s(x1)) = 0
POL(times(x1, x2)) = 1 + x1 + x2
U6_GGA(X1, X2, dcB_out_gga(X1, times(X1, X2), X4)) → DB_IN_GGA(X2, times(X1, X2))
U13_GGA(X1, X2, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, times(X1, X2))
DB_IN_GGA(div(X1, X2), div(X1, X2)) → DB_IN_GGA(times(X1, power(X2, p(0))), div(X1, X2))
U42_GGA(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → DB_IN_GGA(X2, X3)
DB_IN_GGA(power(X1, X2), power(X1, X2)) → U10_GGA(X1, X2, isnumbercA_in_g(X2))
U10_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2))
DB_IN_GGA(power(X1, 0), power(X1, 0)) → DB_IN_GGA(X1, power(X1, 0))
DB_IN_GGA(div(X1, X2), X3) → DB_IN_GGA(times(X1, power(X2, p(0))), X3)
U21_GGA(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(div(X1, X2), X3))
DB_IN_GGA(power(X1, X2), X3) → U46_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(times(power(X1, X2), X3), times(power(X1, X2), X3)) → U24_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U30_GGA(X1, X2, dcB_out_gga(X1, div(X1, X2), X4)) → DB_IN_GGA(power(X2, p(0)), div(X1, X2))
DB_IN_GGA(power(X1, p(X2)), X3) → U74_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2))) → U34_GGA(X1, X2, isnumbercA_in_g(X2))
U34_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)))
U50_GGA(X1, X2, X3, isnumbercA_out_g(X1)) → DB_IN_GGA(X2, X3)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2))) → U37_GGA(X1, X2, isnumbercA_in_g(X2))
U37_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)))
U61_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X4)
DB_IN_GGA(div(X1, X2), X3) → U67_GGA(X1, X2, X3, dcB_in_gga(X1, X3))
DB_IN_GGA(power(X1, 0), X2) → DB_IN_GGA(X1, X2)
DB_IN_GGA(power(X1, s(X2)), X3) → U71_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
U61_GGA(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U63_GGA(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U63_GGA(X1, X2, X3, X4, dcB_out_gga(X1, X4, X6)) → DB_IN_GGA(X3, X4)
U53_GGA(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → U55_GGA(X1, X2, X3, X4, dcB_in_gga(X2, X4))
U24_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → U26_GGA(X1, X2, X3, dcB_in_gga(X1, times(power(X1, X2), X3)))
U18_GGA(X1, X2, X3, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → DB_IN_GGA(X3, times(times(X1, X2), X3))
dcB_in_gga(X1, X1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(times(X1, X2), times(X1, X2)) → U81_gga(X1, X2, dcB_in_gga(X1, times(X1, X2)))
dcB_in_gga(times(X1, X2), times(X1, X2)) → U86_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3)) → U88_gga(X1, X2, X3, dcB_in_gga(X1, times(times(X1, X2), X3)))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3)) → U91_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3)))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3)) → U93_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(0, X1) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2) → U104_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), X2) → U105_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(X1, X2), X3) → U106_gga(X1, X2, X3, dcB_in_gga(X1, X3))
dcB_in_gga(div(X1, X2), X3) → U108_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), X3))
dcB_in_gga(power(X1, X2), X3) → U109_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(times(X1, X2), X1) → U111_gga(X1, X2, dcB_in_gga(X2, X1))
dcB_in_gga(times(X1, X2), X3) → U112_gga(X1, X2, X3, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), X4) → U114_gga(X1, X2, X3, X4, dcB_in_gga(X1, X4))
dcB_in_gga(times(div(X1, X2), X3), X4) → U117_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X4))
dcB_in_gga(times(power(X1, X2), X3), X4) → U119_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0)))) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), X3) → U123_gga(X1, X2, X3, dcB_in_gga(X1, X3))
dcB_in_gga(power(X1, 0), X2) → U125_gga(X1, X2, dcB_in_gga(X1, X2))
dcB_in_gga(power(X1, s(X2)), X3) → U126_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), X3) → U128_gga(X1, X2, X3, isnumbercA_in_g(X2))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
dcB_in_gga(0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1)) → U79_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), p(X1)) → U80_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U83_gga(X1, X2, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2)))
dcB_in_gga(power(X1, X2), power(X1, X2)) → U84_gga(X1, X2, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U97_gga(X1, X2, dcB_in_gga(X1, div(X1, X2)))
dcB_in_gga(power(X1, 0), power(X1, 0)) → U99_gga(X1, dcB_in_gga(X1, power(X1, 0)))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2))) → U100_gga(X1, X2, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2))) → U102_gga(X1, X2, isnumbercA_in_g(X2))
U81_gga(X1, X2, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X4, dcB_in_gga(X2, times(X1, X2)))
U86_gga(X1, X2, isnumbercA_out_g(X1)) → U87_gga(X1, X2, dcB_in_gga(X2, times(X1, X2)))
U88_gga(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X6, dcB_in_gga(X2, times(times(X1, X2), X3)))
U91_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X5, dcB_in_gga(X3, times(div(X1, X2), X3)))
U93_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, dcB_in_gga(X1, times(power(X1, X2), X3)))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
U106_gga(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X5, dcB_in_gga(X2, X3))
U108_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U109_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U111_gga(X1, X2, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U112_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, dcB_in_gga(X2, X3))
U114_gga(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X7, dcB_in_gga(X2, X4))
U117_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X6, dcB_in_gga(X3, X4))
U119_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U123_gga(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X5, dcB_in_gga(power(X2, p(0)), X3))
U125_gga(X1, X2, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U126_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U128_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
U83_gga(X1, X2, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U84_gga(X1, X2, isnumbercA_out_g(X2)) → U85_gga(X1, X2, dcB_in_gga(X1, power(X1, X2)))
U97_gga(X1, X2, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2)))
U99_gga(X1, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U100_gga(X1, X2, isnumbercA_out_g(X2)) → U101_gga(X1, X2, dcB_in_gga(X1, power(X1, s(X2))))
U102_gga(X1, X2, isnumbercA_out_g(X2)) → U103_gga(X1, X2, dcB_in_gga(X1, power(X1, p(X2))))
U82_gga(X1, X2, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
U87_gga(X1, X2, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U89_gga(X1, X2, X3, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3)))
U92_gga(X1, X2, X3, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U94_gga(X1, X2, X3, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X5, dcB_in_gga(X3, times(power(X1, X2), X3)))
U107_gga(X1, X2, X3, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U110_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U113_gga(X1, X2, X3, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U115_gga(X1, X2, X3, X4, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X6, X7, dcB_in_gga(X3, X4))
U118_gga(X1, X2, X3, X4, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U120_gga(X1, X2, X3, X4, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X6, dcB_in_gga(X3, X4))
U124_gga(X1, X2, X3, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U127_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U129_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U85_gga(X1, X2, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U98_gga(X1, X2, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U101_gga(X1, X2, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U103_gga(X1, X2, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U90_gga(X1, X2, X3, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U95_gga(X1, X2, X3, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U116_gga(X1, X2, X3, X4, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U121_gga(X1, X2, X3, X4, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
dcB_in_gga(x0, x1)
isnumbercA_in_g(x0)
U81_gga(x0, x1, x2)
U86_gga(x0, x1, x2)
U88_gga(x0, x1, x2, x3)
U91_gga(x0, x1, x2, x3)
U93_gga(x0, x1, x2, x3)
U104_gga(x0, x1, x2)
U105_gga(x0, x1, x2)
U106_gga(x0, x1, x2, x3)
U108_gga(x0, x1, x2, x3)
U109_gga(x0, x1, x2, x3)
U111_gga(x0, x1, x2)
U112_gga(x0, x1, x2, x3)
U114_gga(x0, x1, x2, x3, x4)
U117_gga(x0, x1, x2, x3, x4)
U119_gga(x0, x1, x2, x3, x4)
U123_gga(x0, x1, x2, x3)
U125_gga(x0, x1, x2)
U126_gga(x0, x1, x2, x3)
U128_gga(x0, x1, x2, x3)
U77_g(x0, x1)
U78_g(x0, x1)
U79_gga(x0, x1)
U80_gga(x0, x1)
U83_gga(x0, x1, x2)
U84_gga(x0, x1, x2)
U97_gga(x0, x1, x2)
U99_gga(x0, x1)
U100_gga(x0, x1, x2)
U102_gga(x0, x1, x2)
U82_gga(x0, x1, x2, x3)
U87_gga(x0, x1, x2)
U89_gga(x0, x1, x2, x3, x4)
U92_gga(x0, x1, x2, x3, x4)
U94_gga(x0, x1, x2, x3)
U107_gga(x0, x1, x2, x3, x4)
U110_gga(x0, x1, x2, x3)
U113_gga(x0, x1, x2, x3)
U115_gga(x0, x1, x2, x3, x4, x5)
U118_gga(x0, x1, x2, x3, x4, x5)
U120_gga(x0, x1, x2, x3, x4)
U124_gga(x0, x1, x2, x3, x4)
U127_gga(x0, x1, x2, x3)
U129_gga(x0, x1, x2, x3)
U85_gga(x0, x1, x2)
U98_gga(x0, x1, x2, x3)
U101_gga(x0, x1, x2)
U103_gga(x0, x1, x2)
U90_gga(x0, x1, x2, x3, x4, x5)
U95_gga(x0, x1, x2, x3, x4)
U116_gga(x0, x1, x2, x3, x4, x5, x6)
U121_gga(x0, x1, x2, x3, x4, x5)
DB_IN_GGA(power(X1, X2), power(X1, X2)) → U10_GGA(X1, X2, isnumbercA_in_g(X2))
U10_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2))
DB_IN_GGA(power(X1, X2), X3) → U46_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, 0), power(X1, 0)) → DB_IN_GGA(X1, power(X1, 0))
DB_IN_GGA(power(X1, p(X2)), X3) → U74_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2))) → U34_GGA(X1, X2, isnumbercA_in_g(X2))
U34_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)))
DB_IN_GGA(power(X1, 0), X2) → DB_IN_GGA(X1, X2)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2))) → U37_GGA(X1, X2, isnumbercA_in_g(X2))
U37_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)))
DB_IN_GGA(power(X1, s(X2)), X3) → U71_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
dcB_in_gga(X1, X1) → dcB_out_gga(X1, X1, 1)
dcB_in_gga(times(X1, X2), times(X1, X2)) → U81_gga(X1, X2, dcB_in_gga(X1, times(X1, X2)))
dcB_in_gga(times(X1, X2), times(X1, X2)) → U86_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), times(times(X1, X2), X3)) → U88_gga(X1, X2, X3, dcB_in_gga(X1, times(times(X1, X2), X3)))
dcB_in_gga(times(div(X1, X2), X3), times(div(X1, X2), X3)) → U91_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3)))
dcB_in_gga(times(power(X1, X2), X3), times(power(X1, X2), X3)) → U93_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(0, X1) → dcB_out_gga(0, X1, 0)
dcB_in_gga(s(X1), X2) → U104_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), X2) → U105_gga(X1, X2, isnumbercA_in_g(X1))
dcB_in_gga(times(X1, X2), X3) → U106_gga(X1, X2, X3, dcB_in_gga(X1, X3))
dcB_in_gga(div(X1, X2), X3) → U108_gga(X1, X2, X3, dcB_in_gga(times(X1, power(X2, p(0))), X3))
dcB_in_gga(power(X1, X2), X3) → U109_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(times(X1, X2), X1) → U111_gga(X1, X2, dcB_in_gga(X2, X1))
dcB_in_gga(times(X1, X2), X3) → U112_gga(X1, X2, X3, isnumbercA_in_g(X1))
dcB_in_gga(times(times(X1, X2), X3), X4) → U114_gga(X1, X2, X3, X4, dcB_in_gga(X1, X4))
dcB_in_gga(times(div(X1, X2), X3), X4) → U117_gga(X1, X2, X3, X4, dcB_in_gga(times(X1, power(X2, p(0))), X4))
dcB_in_gga(times(power(X1, X2), X3), X4) → U119_gga(X1, X2, X3, X4, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), times(X1, power(X2, p(0)))) → dcB_out_gga(div(X1, X2), times(X1, power(X2, p(0))), 1)
dcB_in_gga(div(X1, X2), X3) → U122_gga(X1, X2, X3, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), X3) → U123_gga(X1, X2, X3, dcB_in_gga(X1, X3))
dcB_in_gga(power(X1, 0), X2) → U125_gga(X1, X2, dcB_in_gga(X1, X2))
dcB_in_gga(power(X1, s(X2)), X3) → U126_gga(X1, X2, X3, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), X3) → U128_gga(X1, X2, X3, isnumbercA_in_g(X2))
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
dcB_in_gga(0, 0) → dcB_out_gga(0, 0, 0)
dcB_in_gga(s(X1), s(X1)) → U79_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(p(X1), p(X1)) → U80_gga(X1, isnumbercA_in_g(X1))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U83_gga(X1, X2, dcB_in_gga(times(X1, power(X2, p(0))), div(X1, X2)))
dcB_in_gga(power(X1, X2), power(X1, X2)) → U84_gga(X1, X2, isnumbercA_in_g(X2))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U96_gga(X1, X2, isnumbercA_in_g(times(X1, power(X2, p(0)))))
dcB_in_gga(div(X1, X2), div(X1, X2)) → U97_gga(X1, X2, dcB_in_gga(X1, div(X1, X2)))
dcB_in_gga(power(X1, 0), power(X1, 0)) → U99_gga(X1, dcB_in_gga(X1, power(X1, 0)))
dcB_in_gga(power(X1, s(X2)), power(X1, s(X2))) → U100_gga(X1, X2, isnumbercA_in_g(X2))
dcB_in_gga(power(X1, p(X2)), power(X1, p(X2))) → U102_gga(X1, X2, isnumbercA_in_g(X2))
U81_gga(X1, X2, dcB_out_gga(X1, times(X1, X2), X4)) → U82_gga(X1, X2, X4, dcB_in_gga(X2, times(X1, X2)))
U86_gga(X1, X2, isnumbercA_out_g(X1)) → U87_gga(X1, X2, dcB_in_gga(X2, times(X1, X2)))
U88_gga(X1, X2, X3, dcB_out_gga(X1, times(times(X1, X2), X3), X6)) → U89_gga(X1, X2, X3, X6, dcB_in_gga(X2, times(times(X1, X2), X3)))
U91_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), times(div(X1, X2), X3), X5)) → U92_gga(X1, X2, X3, X5, dcB_in_gga(X3, times(div(X1, X2), X3)))
U93_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U94_gga(X1, X2, X3, dcB_in_gga(X1, times(power(X1, X2), X3)))
U104_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), X2, 0)
U105_gga(X1, X2, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), X2, 0)
U106_gga(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → U107_gga(X1, X2, X3, X5, dcB_in_gga(X2, X3))
U108_gga(X1, X2, X3, dcB_out_gga(times(X1, power(X2, p(0))), X3, X4)) → dcB_out_gga(div(X1, X2), X3, X4)
U109_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U110_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U111_gga(X1, X2, dcB_out_gga(X2, X1, X3)) → dcB_out_gga(times(X1, X2), X1, +(times(X3, X1), times(1, X2)))
U112_gga(X1, X2, X3, isnumbercA_out_g(X1)) → U113_gga(X1, X2, X3, dcB_in_gga(X2, X3))
U114_gga(X1, X2, X3, X4, dcB_out_gga(X1, X4, X7)) → U115_gga(X1, X2, X3, X4, X7, dcB_in_gga(X2, X4))
U117_gga(X1, X2, X3, X4, dcB_out_gga(times(X1, power(X2, p(0))), X4, X6)) → U118_gga(X1, X2, X3, X4, X6, dcB_in_gga(X3, X4))
U119_gga(X1, X2, X3, X4, isnumbercA_out_g(X2)) → U120_gga(X1, X2, X3, X4, dcB_in_gga(X1, X4))
U123_gga(X1, X2, X3, dcB_out_gga(X1, X3, X5)) → U124_gga(X1, X2, X3, X5, dcB_in_gga(power(X2, p(0)), X3))
U125_gga(X1, X2, dcB_out_gga(X1, X2, X3)) → dcB_out_gga(power(X1, 0), X2, times(0, times(X3, power(X1, p(0)))))
U126_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U127_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U128_gga(X1, X2, X3, isnumbercA_out_g(X2)) → U129_gga(X1, X2, X3, dcB_in_gga(X1, X3))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U79_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(s(X1), s(X1), 0)
U80_gga(X1, isnumbercA_out_g(X1)) → dcB_out_gga(p(X1), p(X1), 0)
U83_gga(X1, X2, dcB_out_gga(times(X1, power(X2, p(0))), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), X3)
U84_gga(X1, X2, isnumbercA_out_g(X2)) → U85_gga(X1, X2, dcB_in_gga(X1, power(X1, X2)))
U97_gga(X1, X2, dcB_out_gga(X1, div(X1, X2), X4)) → U98_gga(X1, X2, X4, dcB_in_gga(power(X2, p(0)), div(X1, X2)))
U99_gga(X1, dcB_out_gga(X1, power(X1, 0), X2)) → dcB_out_gga(power(X1, 0), power(X1, 0), times(0, times(X2, power(X1, p(0)))))
U100_gga(X1, X2, isnumbercA_out_g(X2)) → U101_gga(X1, X2, dcB_in_gga(X1, power(X1, s(X2))))
U102_gga(X1, X2, isnumbercA_out_g(X2)) → U103_gga(X1, X2, dcB_in_gga(X1, power(X1, p(X2))))
U82_gga(X1, X2, X4, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(X4, X2)))
U87_gga(X1, X2, dcB_out_gga(X2, times(X1, X2), X3)) → dcB_out_gga(times(X1, X2), times(X1, X2), +(times(X3, X1), times(0, X2)))
U89_gga(X1, X2, X3, X6, dcB_out_gga(X2, times(times(X1, X2), X3), X5)) → U90_gga(X1, X2, X3, X5, X6, dcB_in_gga(X3, times(times(X1, X2), X3)))
U92_gga(X1, X2, X3, X5, dcB_out_gga(X3, times(div(X1, X2), X3), X4)) → dcB_out_gga(times(div(X1, X2), X3), times(div(X1, X2), X3), +(times(X4, div(X1, X2)), times(X5, X3)))
U94_gga(X1, X2, X3, dcB_out_gga(X1, times(power(X1, X2), X3), X5)) → U95_gga(X1, X2, X3, X5, dcB_in_gga(X3, times(power(X1, X2), X3)))
U107_gga(X1, X2, X3, X5, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(X5, X2)))
U110_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, X2), X3, times(X2, times(X4, power(X1, p(X2)))))
U113_gga(X1, X2, X3, dcB_out_gga(X2, X3, X4)) → dcB_out_gga(times(X1, X2), X3, +(times(X4, X1), times(0, X2)))
U115_gga(X1, X2, X3, X4, X7, dcB_out_gga(X2, X4, X6)) → U116_gga(X1, X2, X3, X4, X6, X7, dcB_in_gga(X3, X4))
U118_gga(X1, X2, X3, X4, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(div(X1, X2), X3), X4, +(times(X5, div(X1, X2)), times(X6, X3)))
U120_gga(X1, X2, X3, X4, dcB_out_gga(X1, X4, X6)) → U121_gga(X1, X2, X3, X4, X6, dcB_in_gga(X3, X4))
U124_gga(X1, X2, X3, X5, dcB_out_gga(power(X2, p(0)), X3, X4)) → dcB_out_gga(div(X1, X2), X3, +(times(X4, X1), times(X5, power(X2, p(0)))))
U127_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, s(X2)), X3, times(s(X2), times(X4, power(X1, p(s(X2))))))
U129_gga(X1, X2, X3, dcB_out_gga(X1, X3, X4)) → dcB_out_gga(power(X1, p(X2)), X3, times(p(X2), times(X4, power(X1, p(p(X2))))))
U85_gga(X1, X2, dcB_out_gga(X1, power(X1, X2), X3)) → dcB_out_gga(power(X1, X2), power(X1, X2), times(X2, times(X3, power(X1, p(X2)))))
U98_gga(X1, X2, X4, dcB_out_gga(power(X2, p(0)), div(X1, X2), X3)) → dcB_out_gga(div(X1, X2), div(X1, X2), +(times(X3, X1), times(X4, power(X2, p(0)))))
U101_gga(X1, X2, dcB_out_gga(X1, power(X1, s(X2)), X3)) → dcB_out_gga(power(X1, s(X2)), power(X1, s(X2)), times(s(X2), times(X3, power(X1, p(s(X2))))))
U103_gga(X1, X2, dcB_out_gga(X1, power(X1, p(X2)), X3)) → dcB_out_gga(power(X1, p(X2)), power(X1, p(X2)), times(p(X2), times(X3, power(X1, p(p(X2))))))
U90_gga(X1, X2, X3, X5, X6, dcB_out_gga(X3, times(times(X1, X2), X3), X4)) → dcB_out_gga(times(times(X1, X2), X3), times(times(X1, X2), X3), +(times(X4, times(X1, X2)), times(+(times(X5, X1), times(X6, X2)), X3)))
U95_gga(X1, X2, X3, X5, dcB_out_gga(X3, times(power(X1, X2), X3), X4)) → dcB_out_gga(times(power(X1, X2), X3), times(power(X1, X2), X3), +(times(X4, power(X1, X2)), times(times(X2, times(X5, power(X1, p(X2)))), X3)))
U116_gga(X1, X2, X3, X4, X6, X7, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(times(X1, X2), X3), X4, +(times(X5, times(X1, X2)), times(+(times(X6, X1), times(X7, X2)), X3)))
U121_gga(X1, X2, X3, X4, X6, dcB_out_gga(X3, X4, X5)) → dcB_out_gga(times(power(X1, X2), X3), X4, +(times(X5, power(X1, X2)), times(times(X2, times(X6, power(X1, p(X2)))), X3)))
dcB_in_gga(x0, x1)
isnumbercA_in_g(x0)
U81_gga(x0, x1, x2)
U86_gga(x0, x1, x2)
U88_gga(x0, x1, x2, x3)
U91_gga(x0, x1, x2, x3)
U93_gga(x0, x1, x2, x3)
U104_gga(x0, x1, x2)
U105_gga(x0, x1, x2)
U106_gga(x0, x1, x2, x3)
U108_gga(x0, x1, x2, x3)
U109_gga(x0, x1, x2, x3)
U111_gga(x0, x1, x2)
U112_gga(x0, x1, x2, x3)
U114_gga(x0, x1, x2, x3, x4)
U117_gga(x0, x1, x2, x3, x4)
U119_gga(x0, x1, x2, x3, x4)
U123_gga(x0, x1, x2, x3)
U125_gga(x0, x1, x2)
U126_gga(x0, x1, x2, x3)
U128_gga(x0, x1, x2, x3)
U77_g(x0, x1)
U78_g(x0, x1)
U79_gga(x0, x1)
U80_gga(x0, x1)
U83_gga(x0, x1, x2)
U84_gga(x0, x1, x2)
U97_gga(x0, x1, x2)
U99_gga(x0, x1)
U100_gga(x0, x1, x2)
U102_gga(x0, x1, x2)
U82_gga(x0, x1, x2, x3)
U87_gga(x0, x1, x2)
U89_gga(x0, x1, x2, x3, x4)
U92_gga(x0, x1, x2, x3, x4)
U94_gga(x0, x1, x2, x3)
U107_gga(x0, x1, x2, x3, x4)
U110_gga(x0, x1, x2, x3)
U113_gga(x0, x1, x2, x3)
U115_gga(x0, x1, x2, x3, x4, x5)
U118_gga(x0, x1, x2, x3, x4, x5)
U120_gga(x0, x1, x2, x3, x4)
U124_gga(x0, x1, x2, x3, x4)
U127_gga(x0, x1, x2, x3)
U129_gga(x0, x1, x2, x3)
U85_gga(x0, x1, x2)
U98_gga(x0, x1, x2, x3)
U101_gga(x0, x1, x2)
U103_gga(x0, x1, x2)
U90_gga(x0, x1, x2, x3, x4, x5)
U95_gga(x0, x1, x2, x3, x4)
U116_gga(x0, x1, x2, x3, x4, x5, x6)
U121_gga(x0, x1, x2, x3, x4, x5)
DB_IN_GGA(power(X1, X2), power(X1, X2)) → U10_GGA(X1, X2, isnumbercA_in_g(X2))
U10_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2))
DB_IN_GGA(power(X1, X2), X3) → U46_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, 0), power(X1, 0)) → DB_IN_GGA(X1, power(X1, 0))
DB_IN_GGA(power(X1, p(X2)), X3) → U74_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2))) → U34_GGA(X1, X2, isnumbercA_in_g(X2))
U34_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)))
DB_IN_GGA(power(X1, 0), X2) → DB_IN_GGA(X1, X2)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2))) → U37_GGA(X1, X2, isnumbercA_in_g(X2))
U37_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)))
DB_IN_GGA(power(X1, s(X2)), X3) → U71_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
dcB_in_gga(x0, x1)
isnumbercA_in_g(x0)
U81_gga(x0, x1, x2)
U86_gga(x0, x1, x2)
U88_gga(x0, x1, x2, x3)
U91_gga(x0, x1, x2, x3)
U93_gga(x0, x1, x2, x3)
U104_gga(x0, x1, x2)
U105_gga(x0, x1, x2)
U106_gga(x0, x1, x2, x3)
U108_gga(x0, x1, x2, x3)
U109_gga(x0, x1, x2, x3)
U111_gga(x0, x1, x2)
U112_gga(x0, x1, x2, x3)
U114_gga(x0, x1, x2, x3, x4)
U117_gga(x0, x1, x2, x3, x4)
U119_gga(x0, x1, x2, x3, x4)
U123_gga(x0, x1, x2, x3)
U125_gga(x0, x1, x2)
U126_gga(x0, x1, x2, x3)
U128_gga(x0, x1, x2, x3)
U77_g(x0, x1)
U78_g(x0, x1)
U79_gga(x0, x1)
U80_gga(x0, x1)
U83_gga(x0, x1, x2)
U84_gga(x0, x1, x2)
U97_gga(x0, x1, x2)
U99_gga(x0, x1)
U100_gga(x0, x1, x2)
U102_gga(x0, x1, x2)
U82_gga(x0, x1, x2, x3)
U87_gga(x0, x1, x2)
U89_gga(x0, x1, x2, x3, x4)
U92_gga(x0, x1, x2, x3, x4)
U94_gga(x0, x1, x2, x3)
U107_gga(x0, x1, x2, x3, x4)
U110_gga(x0, x1, x2, x3)
U113_gga(x0, x1, x2, x3)
U115_gga(x0, x1, x2, x3, x4, x5)
U118_gga(x0, x1, x2, x3, x4, x5)
U120_gga(x0, x1, x2, x3, x4)
U124_gga(x0, x1, x2, x3, x4)
U127_gga(x0, x1, x2, x3)
U129_gga(x0, x1, x2, x3)
U85_gga(x0, x1, x2)
U98_gga(x0, x1, x2, x3)
U101_gga(x0, x1, x2)
U103_gga(x0, x1, x2)
U90_gga(x0, x1, x2, x3, x4, x5)
U95_gga(x0, x1, x2, x3, x4)
U116_gga(x0, x1, x2, x3, x4, x5, x6)
U121_gga(x0, x1, x2, x3, x4, x5)
dcB_in_gga(x0, x1)
U81_gga(x0, x1, x2)
U86_gga(x0, x1, x2)
U88_gga(x0, x1, x2, x3)
U91_gga(x0, x1, x2, x3)
U93_gga(x0, x1, x2, x3)
U104_gga(x0, x1, x2)
U105_gga(x0, x1, x2)
U106_gga(x0, x1, x2, x3)
U108_gga(x0, x1, x2, x3)
U109_gga(x0, x1, x2, x3)
U111_gga(x0, x1, x2)
U112_gga(x0, x1, x2, x3)
U114_gga(x0, x1, x2, x3, x4)
U117_gga(x0, x1, x2, x3, x4)
U119_gga(x0, x1, x2, x3, x4)
U123_gga(x0, x1, x2, x3)
U125_gga(x0, x1, x2)
U126_gga(x0, x1, x2, x3)
U128_gga(x0, x1, x2, x3)
U79_gga(x0, x1)
U80_gga(x0, x1)
U83_gga(x0, x1, x2)
U84_gga(x0, x1, x2)
U97_gga(x0, x1, x2)
U99_gga(x0, x1)
U100_gga(x0, x1, x2)
U102_gga(x0, x1, x2)
U82_gga(x0, x1, x2, x3)
U87_gga(x0, x1, x2)
U89_gga(x0, x1, x2, x3, x4)
U92_gga(x0, x1, x2, x3, x4)
U94_gga(x0, x1, x2, x3)
U107_gga(x0, x1, x2, x3, x4)
U110_gga(x0, x1, x2, x3)
U113_gga(x0, x1, x2, x3)
U115_gga(x0, x1, x2, x3, x4, x5)
U118_gga(x0, x1, x2, x3, x4, x5)
U120_gga(x0, x1, x2, x3, x4)
U124_gga(x0, x1, x2, x3, x4)
U127_gga(x0, x1, x2, x3)
U129_gga(x0, x1, x2, x3)
U85_gga(x0, x1, x2)
U98_gga(x0, x1, x2, x3)
U101_gga(x0, x1, x2)
U103_gga(x0, x1, x2)
U90_gga(x0, x1, x2, x3, x4, x5)
U95_gga(x0, x1, x2, x3, x4)
U116_gga(x0, x1, x2, x3, x4, x5, x6)
U121_gga(x0, x1, x2, x3, x4, x5)
DB_IN_GGA(power(X1, X2), power(X1, X2)) → U10_GGA(X1, X2, isnumbercA_in_g(X2))
U10_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, X2))
DB_IN_GGA(power(X1, X2), X3) → U46_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U46_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, 0), power(X1, 0)) → DB_IN_GGA(X1, power(X1, 0))
DB_IN_GGA(power(X1, p(X2)), X3) → U74_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U74_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
DB_IN_GGA(power(X1, s(X2)), power(X1, s(X2))) → U34_GGA(X1, X2, isnumbercA_in_g(X2))
U34_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, s(X2)))
DB_IN_GGA(power(X1, 0), X2) → DB_IN_GGA(X1, X2)
DB_IN_GGA(power(X1, p(X2)), power(X1, p(X2))) → U37_GGA(X1, X2, isnumbercA_in_g(X2))
U37_GGA(X1, X2, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, power(X1, p(X2)))
DB_IN_GGA(power(X1, s(X2)), X3) → U71_GGA(X1, X2, X3, isnumbercA_in_g(X2))
U71_GGA(X1, X2, X3, isnumbercA_out_g(X2)) → DB_IN_GGA(X1, X3)
isnumbercA_in_g(0) → isnumbercA_out_g(0)
isnumbercA_in_g(s(X1)) → U77_g(X1, isnumbercA_in_g(X1))
isnumbercA_in_g(p(X1)) → U78_g(X1, isnumbercA_in_g(X1))
U78_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(p(X1))
U77_g(X1, isnumbercA_out_g(X1)) → isnumbercA_out_g(s(X1))
isnumbercA_in_g(x0)
U77_g(x0, x1)
U78_g(x0, x1)
From the DPs we obtained the following set of size-change graphs: